Conventionally, for hardware (circuits) designed to realize a given function, logical verification is requisite as a pre-process of actual hardware manufacture to detect omissions in the design. Specifically, logical verification is performed using output that results from an input of verification scenarios generated according to the design of the hardware (see, for example, Japanese Laid-Open Patent Publication Nos. 2006-190209, 2006-201980; and Foster, Harry D., et al, “Programming Code Metrics”, Assertion-Based Design (2nd Edition), 2004, pp. 129-130).
Verification coverage is calculated to objectively evaluate the verification performed by the verification scenario generated as described above. Verification coverage provides an index of whether patterns for simulation verification of a target are sufficient. Verification coverage is, for example, a coverage rate that is the ratio of the number of executed patterns for simulation verification to the population constituted by all patterns of simulation verification to be verified. In this case, it is expected that the higher the verification coverage (coverage rate) is, the higher the verification accuracy becomes.
However, a problem here is how to extract “all patterns of simulation verification to be verified” that constitute the population. All patterns of simulation verification corresponding to the population are referred to as coverage reference. If patterns that are actually useless in the verification are extracted as the coverage reference, a higher coverage rate of simulation verification does not necessarily improve the actual efficiency of verification.
Thus, a method of extracting all patterns according to specific criteria, such as path coverage and code coverage, is currently used. Path coverage is patterns for verifying all paths in which state transition occurs in registers included in a target circuit. Thus, the sum of these patterns becomes the coverage reference in path coverage. Code coverage is also referred to as line coverage, and is patterns for verifying paths concerning input/output of registers described in a source code corresponding to the target circuit. Similarly, the sum of these patterns becomes the coverage reference in code coverage.
However, a bug due to an omission in verification can occur during actual operation of the circuit even if verification has been performed using verification scenarios that cover the coverage reference described above. This is because even a verification scenario having a coverage reference of 100% may miss verifying a branch condition within the circuit.
FIG. 17 depicts an example in which an error in a conditional branch is missed. For example, in designing hardware (circuit) according to a specification that specifies “condition A>condition B” as a priority of implementation, a correct statement 1710 according to the specification may be changed to an erroneous statement 1720 as depicted in FIG. 17 consequent to, for example, an erroneous correction by a designer. In the correct statement 1710, an if statement 1712 for condition B is further described within an if statement 1711 for condition A.
On the other hand, in the erroneous statement 1720, an if statement 1722 for condition A is described within an if statement 1721 for condition B. Thus, the erroneous statement 1720 represents “condition B>condition A,” which contradicts the implementation intended and specified by the specification.
However, with the coverage reference described above, it is possible that a description error such as the erroneous statement 1720 is missed in at verification. FIG. 18 depicts a chart comparing the correct statement and the erroneous statement. With reference to FIG. 18, examples are described in which the correct statement 1710 and the erroneous statement 1720 are executed, respectively.
As depicted in a chart 1800 of FIG. 18, comparison of the correct statement 1710 and the erroneous statement 1720 indicates that four patterns 1801 are executed according to the evaluation result (Yes/No) of each condition. Among the four patterns 1801, for three patterns 1802 in which condition A and condition B are not satisfied (Yes) at the same time, what is executed is the same for both the correct statement 1710 and the erroneous statement 1720. On the other hand, what is executed becomes different only for a pattern 1803 in which condition A and condition B are satisfied at the same time.
FIG. 19 depicts an exemplary verification scenario with a line coverage of 100%. If the subject of verification is the correct statement 1710, for the pattern (No, No) of a verification scenario 1900 in which neither condition A nor condition B is satisfied, a process c described at the deepest position (in the bottom layer) of the correct statement 1710 is verified.
For the pattern (No, Yes) in which only condition B is satisfied, a process b in the correct statement 1710 is verified. For the pattern (Yes, No) in which only condition A is satisfied, a process a described at the shallowest position of the correct statement 1710 is verified.
Consequently, all statements of the correct statement 1710 are included in the coverage area of the verification scenario as depicted in FIG. 19. Thus, in line coverage, the coverage (coverage rate) becomes 100% without verifying the pattern (Yes, Yes) in which condition A and condition B are both satisfied.
When the path coverage described above is taken as the coverage reference, a path of the pattern (Yes, Yes) in which condition A and condition B are both satisfied does not exist in the correct statement 1710, and naturally is excluded from the population of the coverage reference. Thus, similar to the line coverage, the coverage (coverage rate) becomes 100% without verifying the pattern (Yes, Yes) in which condition A and condition B are both satisfied.
As described above, with the conventional coverage reference, it is possible for the coverage concerning conditional branches within the target circuit to not be entirely covered, even if a verification scenario having the coverage rate of 100% is generated. Nonetheless, there has been provided no technology for checking whether the coverage concerning conditional branches is covered by the generated verification scenario. Consequently, verification cannot extract an inclusion of the erroneous statement 1720 described in FIG. 17 as a problem, resulting in a hardware design that includes a bug.
Further, various specifications are generally set for processes included in hardware description. When a conditional branch statement includes several condition expressions, for example, a priority in the order of execution and/or exclusivity of the condition expressions are set. A priority may be set such as “condition expression A>condition expression B>condition expression C”, where the order of execution has to give priority to a higher condition expression.
To be exclusive means that target conditions are not satisfied at the same time. For example, if condition expression A and condition expression B are listed as target conditions and are set to be exclusive, a corresponding process has to be such that condition expression A and condition expression B are not satisfied at the same time. Specifically, a process in which condition expression A=1 and condition expression B=1 is excluded.
Verification without omission becomes more difficult when the specifications such as those described above are set. If no exclusivity is set, by creating a verification scenario that causes the condition expressions to be executed in order of priority, verification without omission is possible even for a conditional branch statement that includes, for example, three or more condition expressions. However, if exclusivity is set for the condition expressions, a verification scenario is omitted for a case in which the condition expressions are not satisfied at the same time, resulting in an omission in verification.